finite-type() 

latex

Definitions	, (x  l), P  Q, t  T, x:A. B(x), Prop, P  Q, P  Q, P & Q, P  Q, b, A, b, Unit, x:A. B(x), false, true, {T}
Lemmas	finite-type-iff-list, eqtt to assert, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, iff transitivity, or functionality wrt iff, cons member, l member wf, btrue wf, bool wf, bfalse wf